proof(L3): add T_Echo_L1 typing rule for runtime echo values (slice 3a)#192
Merged
hyperpolymath merged 1 commit intoMay 27, 2026
Merged
Conversation
Slice 3a of the L3 wiring sequence. Slices 1 + 2 (PRs #190, #191) added the AST surface and the observation consumer; this slice closes the typing for the runtime echo VALUE form so that the forthcoming step rules (S_Region_Exit_Echo, S_Drop_Echo — slice 3b) have a type-preserving target. Changes (formal/TypingL1.v) * New typing rule T_Echo_L1 : has_type_l1 m R G (EEcho T v) (TEcho T) R G when [is_value v] and [has_type_l1 m R G v T R G]. Modality- polymorphic. Echoes are runtime values that preserve both R and G (no resource state change at the typing layer), mirroring T_Borrow_Val_L1's value-of-value pattern. Cascade fixes (formal/Semantics_L1.v) * value_R_G_preserving_l1 VEcho case: was [inversion Ht] expecting vacuity; now inverts to T_Echo_L1 which gives R_out = R and G_out = G directly. * shift_typing_gen_l1_m: explicit T_Echo_L1 bullet (uses shift_preserves_value for the value premise + IH for the witness typing). * subst_typing_gen_l1_m: explicit T_Echo_L1 bullet (uses subst_preserves_value + IH). * region_shrink_preserves_typing_l1_gen_m: explicit T_Echo_L1 bullet before Admitted (closes via IH on the witness; the is_value premise is preserved by structure). The new constructor's insertion BEFORE T_Observe_L1 in the inductive declaration shifted the bullet indices in three proofs; each now has the matching T_Echo_L1 bullet. What is NOT in this slice (still deferred) * S_Region_Exit_Echo / S_Drop_Echo step rules in Semantics.v (slice 3b — parallel-rule strategy approved by owner). * T_Region_L1_Echo / T_Drop_L1_Echo (parallel typing rules matching the new step-rule output type) — slice 3b. * G (echo context) threading through compound rules — slice 3c. * preservation_l3 — slice 4. Build oracle * coqc 8.18.0 closes the full formal/ tree. * Net debt unchanged (3 Admitted in Semantics_L1.v, all pre-existing). Refs PROOF-NEEDS.md §2 (L3 wiring). Refs PRESERVATION-DESIGN.md §6.3. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
2 tasks
hyperpolymath
added a commit
that referenced
this pull request
May 27, 2026
## Summary The original PROOF-NEEDS.md §2 task \"thread G (echo context) alongside R through compound rules\" was speculative — the design question was whether L3 wiring would need a NEW context parameter on every \`has_type_l1\` constructor. Under the **owner-approved parallel-rules design** landed via slices 3a–3c ([#192](../pull/192), [#193](../pull/193), [#194](../pull/194)): - Echoes are runtime VALUES of type \`TEcho T\` (slice 1 + 3a). - They flow through the EXISTING \`ctx\` G context like any other value — no new context parameter needed. - \`T_Observe_L1\` consumes them like any ordinary expression (slice 2). - The two paths (legacy + echo-aware) coexist via parallel typing/step rules, not via context augmentation (slices 3b + 3c). So the G-threading task is **OBSOLETE**. PROOF-NEEDS.md §2 updated to mark it struck-through with explanation. The L3 wiring sequence proceeds directly from 3c to slice 4 (\`preservation_l3\` capstone). ## No code changes Documentation-only update to PROOF-NEEDS.md §2. ## Refs - PROOF-NEEDS.md §2 (L3 wiring) - PRs #192, #193, #194 for the prerequisite slices that obviated this task - PRESERVATION-DESIGN.md §6.3 (L3 design) ## Test plan - [x] No code changes (docs-only) - [ ] CI governance / language-policy passes 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Slice 3a of the L3 wiring sequence. Slices 1 (#190) and 2 (#191) added the AST surface and the observation consumer; this slice closes the typing for the runtime echo VALUE form so that the forthcoming step rules (`S_Region_Exit_Echo`, `S_Drop_Echo` — slice 3b) have a type-preserving target.
Changes (formal/TypingL1.v)
New typing rule:
```coq
T_Echo_L1 : forall m R G v T,
is_value v ->
R; G |=L1[m] v : T -| R; G ->
R; G |=L1[m] EEcho T v : TEcho T -| R; G
```
Modality-polymorphic. Echoes are runtime values that preserve both `R` and `G` (no resource state change at the typing layer), mirroring `T_Borrow_Val_L1`'s value-of-value pattern.
Cascade fixes (formal/Semantics_L1.v)
The new constructor's insertion before `T_Observe_L1` in the inductive declaration shifted the bullet indices in three proofs; each now has the matching `T_Echo_L1` bullet.
What is NOT in this slice (still deferred)
Build oracle
Refs
Test plan
🤖 Generated with Claude Code